perm filename BOYERM.XGP[LET,JMC] blob sn#763073 filedate 1984-08-01 generic text, type T, neo UTF8
/LMAR=0/XLINE=3/FONT#0=BASL30/FONT#1=BASI30/FONT#2=BASB30/FONT#10=BAXM30/FONT#11=ZERO30/FONT#3=STA200/FONT#4=NGB25
␈↓ ↓H␈↓␈↓βS␈↓∧ Department of Computer Science, STANFORD UNIVERSITY, Stanford, California 94305

␈↓ ↓H␈↓∧Telephone: 415 497-4430␈↓ 

August 1, 1984 

␈↓ ↓H␈↓∧Electronic mail: JMC␈↓@␈↓∧SU-AI␈↓
.␈↓∧ARPA




␈↓ ↓H␈↓Professor K. Mani Chandy
␈↓ ↓H␈↓Dept. of Computer Sciences
␈↓ ↓H␈↓University of Texas
␈↓ ↓H␈↓Austin, TX 78712-1188

␈↓ ↓H␈↓Dear Professor Chandy:

␈↓ ↓H␈↓        Sorry␈α⊂for␈α∂the␈α⊂long␈α∂delay␈α⊂in␈α⊂the␈α∂letter␈α⊂about␈α∂Boyer␈α⊂and␈α⊂Moore.␈α∂ I␈α⊂was␈α∂hoping␈α⊂to␈α⊂≡nd␈α∂a
␈↓ ↓H␈↓previous letter I thought I had written so I could update it.

␈↓ ↓H␈↓        I␈α
think␈αBoyer␈α
and␈αMoore␈α
have␈αdone␈α
the␈αbest␈α
work␈αin␈α
automated␈αtheorem␈α
proving.␈α It's␈α
best,
␈↓ ↓H␈↓because␈α⊃almost␈α⊃everyone␈α⊂else␈α⊃has␈α⊃shirked␈α⊃the␈α⊂problem␈α⊃of␈α⊃generating␈α⊃mathematical␈α⊂inductions.
␈↓ ↓H␈↓Moreover, they have applied their methods to a wider variety of problems than other workers.

␈↓ ↓H␈↓        Their␈α∞productivity␈α∞seems␈α
to␈α∞have␈α∞increased␈α
since␈α∞they␈α∞moved␈α
to␈α∞the␈α∞University␈α∞of␈α
Texas,
␈↓ ↓H␈↓and␈α
several␈α
students␈α∞have␈α
broken␈α
new␈α∞ground␈α
in␈α
using␈α
their␈α∞system␈α
for␈α
mathematical␈α∞proofs.␈α
 I
␈↓ ↓H␈↓have in mind in particular the proof of Gauss's law of quadratic reciprocity.

␈↓ ↓H␈↓        Finally,␈α⊃they␈α⊃have␈α⊃published␈α⊃regularly␈α⊃and␈α⊃informtively.␈α⊃ I␈α⊃believe␈α⊃their␈α⊃work␈α∩is␈α⊃better
␈↓ ↓H␈↓described␈α∞in␈α
papers␈α∞and␈α
books␈α∞than␈α
anyone␈α∞else's.␈α
 Supe≡nally,␈α∞their␈α
programs␈α∞have␈α∞been␈α
made
␈↓ ↓H␈↓available in Interlisp, Maclisp and Lisp Machine Lisp to anyone who wants them.

␈↓ ↓H␈↓        In short I think there is an ideal case for making them full professors.


␈↓ ↓H␈↓Sincerely,



␈↓ ↓H␈↓John McCarthy
␈↓ ↓H␈↓Professor of Computer Science